$i$ = $j$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$eqof(IdDeq)($i$,$j$)